(*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

theory MultByAdd
imports
  "AutoCorres.AutoCorres"
begin

(* Parse the input file. *)
external_file "mult_by_add.c"
install_C_file "mult_by_add.c"

(* Abstract the input file. *)
autocorres [ ts_force nondet = mult_by_add ] "mult_by_add.c"

context mult_by_add begin

(*
 * Prove the function returns the correct result, and (simultaneously)
 * does not fail and terminates.
 *)
lemma "\<lbrace> \<lambda>s. True \<rbrace> mult_by_add' a b \<lbrace> \<lambda>r s. r = a * b \<rbrace>!"
  (* Unfold function definition. *)
  apply (clarsimp simp: mult_by_add'_def)

  (* Annotate while loop with an invariant and measure. *)
  apply (subst whileLoop_add_inv
    [where I="\<lambda>(a', r) s. (a' * b) + r = (a * b)"
       and M="\<lambda>((a', _), s). unat a'"])

  (* Run "wp" weakest precondition tactic, and solve verification *
   * conditions generated by it. *)
  apply wp
     apply (simp add: field_simps)
    apply unat_arith
   apply (simp add: split_def word_neq_0_conv[symmetric])
  apply (simp add: split_def | wp)+
  done

(*
 * Equivalent partial-correctness proof using Simpl framework.
 *)
lemma "\<Gamma> \<turnstile> {s. s = t} \<acute>ret__unsigned :== CALL mult_by_add(\<acute>a, \<acute>b) \<lbrace> (\<acute>ret__unsigned = \<^bsup>t\<^esup>a * \<^bsup>t\<^esup>b) \<rbrace>"
  (* Unfold the body. *)
  apply vcg_step
   defer

   (* Annotate the while loop with an invariant and variant. *)
   apply (subst whileAnno_def)
   apply (subst whileAnno_def [symmetric,
     where I=" \<lbrace> (\<acute>a * \<acute>b + \<acute>result) = (\<^bsup>t\<^esup>a * \<^bsup>t\<^esup>b) \<rbrace>"
     and V="measure (\<lambda>s. unat (a_' s))"])

  (* Solve the remaining conditions. *)
   apply vcg
   apply (fastforce intro: unat_mono simp: gt0_iff_gem1 field_simps less_1_simp scast_id)+
  done

end

end
